// SPDX-FileCopyrightText: 2023-2025 CASTest Corporation Limited
// SPDX-FileCopyrightText: 2023-2025 Institute of Computing Technology, Chinese Academy of Sciences
// SPDX-License-Identifier: LGPL-v3

#ifndef ICTEST_SAFTEST_H
#define ICTEST_SAFTEST_H

#include "ATPGCommons.h"
#include "SplitDecisionTree.h"

namespace ictest {

// ATPG核心代码，基于D算法
class SAFTest : public ATPGCommons {
public:
  SAFTest(PrimNetlist *prim, SimEngine *sim) {
    prim_ = prim;
    sim_ = sim;
  }

  ~SAFTest() {
    delete driven_table_;
    delete dec_tree_;
    for (auto fanout_region : free_fanout_regions_) {
      delete fanout_region;
    }
  }

  void InitSAFTestStatus();

  void ResetSAFTestStatus();

  void MarkFaultCone();

  void FindFaultSupportRegion();

  bool InjectFaultEffectAndMandatory();

  int TestGen(SAF *target_fault, int max_allowed_backtracks);

  // Decision making.
  bool MakeDecision(SplitSiblingTreeNode *dec_node);

  bool Backtrack();

  std::vector<std::pair<Gate *, Gate *>>
  PathOfTransitiveFanout(Gate *last_path);

  void EliminateUnjustified(
      std::vector<std::pair<Gate *, uint8_t>> &unjustified, bool is_good);

  void
  AddToChildrenUnjustified(SplitSiblingTreeNode *dec_node,
                           std::vector<std::pair<Gate *, uint8_t>> &uj_good,
                           std::vector<std::pair<Gate *, uint8_t>> &uj_bad);

  void AddToChildrenPropagation(SplitSiblingTreeNode *dec_node, Gate *dec_gate);

  static void MergeImplications(std::vector<Gate *> &imply_good,
                                std::vector<Gate *> &imply_bad,
                                std::vector<Gate *> &imply_good_new,
                                std::vector<Gate *> &imply_bad_new);

  void AddImplicationsToNode(std::vector<Gate *> &imply_good,
                             std::vector<Gate *> &imply_bad,
                             SplitSiblingTreeNode *dec_node);

  // Implications.
  bool Imply(std::vector<Gate *> &imply_good, std::vector<Gate *> &imply_bad,
             std::vector<std::pair<Gate *, uint8_t>> &uj_good,
             std::vector<std::pair<Gate *, uint8_t>> &uj_bad);

  std::vector<std::pair<bool, std::pair<Gate *, uint8_t>>>
  BackwardImply(Gate *backward_gate, uint8_t backward_val,
                bool backward_gate_is_good);

  inline int GetGateValue(Gate *gate, bool is_good);

  inline bool TargetImplyIsGood(Gate *gate, bool is_good);

  void AssignImplyValue(Gate *gate, uint8_t val, bool is_good,
                        std::vector<Gate *> &imply_good,
                        std::vector<Gate *> &imply_bad,
                        std::vector<std::pair<Gate *, bool>> &imply_queue);

  void AssignGateValue(Gate *gate, uint8_t val, bool is_good);

  void ResetImply(std::vector<Gate *> &imply_good,
                  std::vector<Gate *> &imply_bad);

  int EvalGate(Gate *gate, bool is_good);

  inline bool OutFaultCone(const int &gate_id);

  void ImplyATPGConstraints();

public:
  std::vector<int> good_;
  std::vector<int> bad_;

  int backtracks_;
  int total_backtracks_;
  int max_backtracks_;
  int max_allowed_backtracks_;
  int atpg_invokes_;

private:
  SAF *fault_under_test_;
  Gate *faulty_gate_;

  std::vector<SplitSiblingTreeNode *> dec_stack_;
  SplitDecisionTree *dec_tree_;
  LogicDrivenTable *driven_table_;
  std::vector<int> fault_cone_;
  bool fault_observed_;

  std::vector<std::pair<Gate *, bool>> imply_queue_;
  std::vector<int> atpg_constrain_value_;
  bool pre_imply_;
};
} // namespace ictest

#endif // ICTEST_SAFTEST_H
